YES 0.99 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/List.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:



↳ HASKELL
  ↳ BR

mainModule List
  ((genericDrop :: Int  ->  [a]  ->  [a]) :: Int  ->  [a]  ->  [a])

module List where
  import qualified Maybe
import qualified Prelude
  genericDrop :: Integral a => a  ->  [b]  ->  [b]
genericDrop 0 xs = xs
genericDrop _ [] = []
genericDrop n (_ : xs) 
 | n > 0 = 
genericDrop (n - 1) xs
genericDrop _ _ = error []


module Maybe where
  import qualified List
import qualified Prelude


Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR

mainModule List
  ((genericDrop :: Int  ->  [a]  ->  [a]) :: Int  ->  [a]  ->  [a])

module List where
  import qualified Maybe
import qualified Prelude
  genericDrop :: Integral b => b  ->  [a]  ->  [a]
genericDrop 0 xs = xs
genericDrop vw [] = []
genericDrop n (vx : xs) 
 | n > 0 = 
genericDrop (n - 1) xs
genericDrop vy vz = error []


module Maybe where
  import qualified List
import qualified Prelude


Cond Reductions:
The following Function with conditions
genericDrop 0 xs = xs
genericDrop vw [] = []
genericDrop n (vx : xs)
 | n > 0
 = genericDrop (n - 1) xs
genericDrop vy vz = error []

is transformed to
genericDrop zu xs = genericDrop5 zu xs
genericDrop vw [] = genericDrop3 vw []
genericDrop n (vx : xs) = genericDrop2 n (vx : xs)
genericDrop vy vz = genericDrop0 vy vz

genericDrop0 vy vz = error []

genericDrop1 n vx xs True = genericDrop (n - 1) xs
genericDrop1 n vx xs False = genericDrop0 n (vx : xs)

genericDrop2 n (vx : xs) = genericDrop1 n vx xs (n > 0)
genericDrop2 yv yw = genericDrop0 yv yw

genericDrop3 vw [] = []
genericDrop3 yy yz = genericDrop2 yy yz

genericDrop4 True zu xs = xs
genericDrop4 zv zw zx = genericDrop3 zw zx

genericDrop5 zu xs = genericDrop4 (zu == 0) zu xs
genericDrop5 zy zz = genericDrop3 zy zz

The following Function with conditions
undefined 
 | False
 = undefined

is transformed to
undefined  = undefined1

undefined0 True = undefined

undefined1  = undefined0 False



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ NumRed

mainModule List
  ((genericDrop :: Int  ->  [a]  ->  [a]) :: Int  ->  [a]  ->  [a])

module List where
  import qualified Maybe
import qualified Prelude
  genericDrop :: Integral b => b  ->  [a]  ->  [a]
genericDrop zu xs = genericDrop5 zu xs
genericDrop vw [] = genericDrop3 vw []
genericDrop n (vx : xs) = genericDrop2 n (vx : xs)
genericDrop vy vz = genericDrop0 vy vz

  
genericDrop0 vy vz = error []

  
genericDrop1 n vx xs True = genericDrop (n - 1) xs
genericDrop1 n vx xs False = genericDrop0 n (vx : xs)

  
genericDrop2 n (vx : xs) = genericDrop1 n vx xs (n > 0)
genericDrop2 yv yw = genericDrop0 yv yw

  
genericDrop3 vw [] = []
genericDrop3 yy yz = genericDrop2 yy yz

  
genericDrop4 True zu xs = xs
genericDrop4 zv zw zx = genericDrop3 zw zx

  
genericDrop5 zu xs = genericDrop4 (zu == 0) zu xs
genericDrop5 zy zz = genericDrop3 zy zz


module Maybe where
  import qualified List
import qualified Prelude


Num Reduction: All numbers are transformed to thier corresponding representation with Pos, Neg, Succ and Zero.

↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ NumRed
            ↳ HASKELL
              ↳ Narrow

mainModule List
  (genericDrop :: Int  ->  [a]  ->  [a])

module List where
  import qualified Maybe
import qualified Prelude
  genericDrop :: Integral b => b  ->  [a]  ->  [a]
genericDrop zu xs = genericDrop5 zu xs
genericDrop vw [] = genericDrop3 vw []
genericDrop n (vx : xs) = genericDrop2 n (vx : xs)
genericDrop vy vz = genericDrop0 vy vz

  
genericDrop0 vy vz = error []

  
genericDrop1 n vx xs True = genericDrop (n - fromInt (Pos (Succ Zero))) xs
genericDrop1 n vx xs False = genericDrop0 n (vx : xs)

  
genericDrop2 n (vx : xs) = genericDrop1 n vx xs (n > fromInt (Pos Zero))
genericDrop2 yv yw = genericDrop0 yv yw

  
genericDrop3 vw [] = []
genericDrop3 yy yz = genericDrop2 yy yz

  
genericDrop4 True zu xs = xs
genericDrop4 zv zw zx = genericDrop3 zw zx

  
genericDrop5 zu xs = genericDrop4 (zu == fromInt (Pos Zero)) zu xs
genericDrop5 zy zz = genericDrop3 zy zz


module Maybe where
  import qualified List
import qualified Prelude


Haskell To QDPs


↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ NumRed
            ↳ HASKELL
              ↳ Narrow
                ↳ QDP
                  ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

new_genericDrop(Pos(Succ(vuu300)), :(vuu40, vuu41), ba) → new_genericDrop(new_primMinusNat(vuu300), vuu41, ba)

The TRS R consists of the following rules:

new_primMinusNat(Succ(vuu3000)) → Pos(Succ(vuu3000))
new_primMinusNat(Zero) → Pos(Zero)

The set Q consists of the following terms:

new_primMinusNat(Succ(x0))
new_primMinusNat(Zero)

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: